perm filename S22[1,JRA] blob
sn#011375 filedate 1972-11-10 generic text, type T, neo UTF8
00100 PRE_OP:J,C,M,N;
00200 PRE_PRED:P,R,Q;
00300 VAR:X1,X2,X3,X4;
01700 ∀(X1,X2,X3,X4) ((((P(X1,X2)∨P(X2,X1))∧(P(X3,X4)∨P(X4,X3)))∧
01800 ((P(X1,X2)∧P(X3,X4))→Q(J(M(N,X3),M(C(N),X2)),J(M(N,X1),M(C(N),X4))))
02000 ∧ ((P(X2,X1)∧P(X4,X3))→Q(J(M(N,X4),M(C(N),X1)),J(M(N,X2),M(C(N),X3))))
02100 ∧ ((P(X2,X1)∧P(X3,X4))→Q(J(M(N,X3),M(C(N),X1)),J(M(N,X2),M(C(N),X4)))))
02200 →R(X1,X2,X3,X4));;
02300 ∀(X1,X2,X3,X4) (R(X1,X2,X3,X4)∨R(X3,X4,X1,X2));;